<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>seL4 Project Roadmap | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/">
              <span property="name"><b>Projects</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">seL4 Project Roadmap</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    


<div class="sidebar">



      <ul class="nav nav-sidebar">
  
        <li class="">
          <a class="" href="/Resources.html">
            Resources
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/documentation.html">
            seL4 Documentation
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/frequently-asked-questions.html">
            seL4 FAQ
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/buildsystem/host-dependencies.html">
            Set up your machine
          </a>
        </li>
  
        <li class="">
          <a class="" href="/Hardware/">
            Supported platforms
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/available-user-components.html">
            Available components
          </a>
        </li>
  
        <li class="active">
          <a class="" href="/projects/roadmap.html">
            Roadmap
          </a>
        </li>
  
        <li class="">
          <a class="" href="/CommunityProjects.html">
            Community projects
          </a>
        </li>
  
        <li class="">
          <a class="" href="/releases/sel4">
            Release Notes
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/api-doc.html">
            libsel4 API
          </a>
        </li>
  
        <li class="">
          <a class="" href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">
            Current Manual
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/verified-configurations.html">
            Verified Configurations
          </a>
        </li>
  
      </ul>














</div>

  </div>
  <div class="api content col-sm-8 col-md-6 col-lg-7 main">
    <h1 id="sel4-project-roadmap">seL4 Project Roadmap</h1>

<p>The seL4 project roadmap lists larger planned contributions to the seL4
ecosystem, such as new architecture ports, new large formal verifications,
large or fundamental new features, user-level frameworks, or components with
general interest to the community.</p>

<p>The purpose is to provide a timeline to the community of when larger
contributions will become available with a reasonable level of commitment,
and for contributors to advertise to others which larger contributions they
are working on.</p>

<p>Features that are <em>in progress</em> are currently being worked on, features that
are <em>planned</em> have not yet had work started on them.</p>

<p>To put a feature on the roadmap, the respective contributor will have made a
commitment to delivering it, but these are not contracts — <strong>any dates
are indicative and subject to change!</strong></p>

<p>Some features may become available in experimental preview <em>branches</em> before
they are merged into the <em>master</em> branch. The dates in the table are for the
completion of the feature in <em>master</em>. The preview branches may undergo
significant changes before they are merged and may also be abandoned. Some of
these branches may be long-lived, because features can only be merged into
<em>master</em> when they are either formally verified or do not affect the verified
configurations of the kernel. Typically, while a larger feature undergoes
formal verification, it will be available in a branch or a non-verified
configuration. Such features often undergo smaller API-level changes while
the verification progresses and either finds flaws or otherwise influences
the design.</p>

<p>In many cases, the roadmap could be accelerated with more funding for the
contributors who work on them, or, in some cases, by volunteering time. If
you are interested, talk to the <a href="https://sel4.systems/Foundation/About" title="seL4 Foundation">seL4 Foundation</a> or directly to foundation
members, e.g. when it involves formal verification to <a href="https://proofcraft.systems" title="Proofcraft">Proofcraft</a> or for
major seL4 kernel features to the <a href="https://trustworthy.systems" title="Trustworthy Systems">Trustworthy Systems</a> group.</p>

<h2 id="sel4-development">seL4 Development</h2>

<!-- Draws content from the "roadmap" section in /_data/projects/<project>.yml -->

<table class="table">
    <thead>
        <tr>
            <th>Feature</th>
            <th>Description</th>
            <th>Assigned</th>
            <th>Status</th>
        </tr>
    </thead>
    <tbody>
        <tr class="">
            <td>MCS Kernel extensions</td>
            <td>A new scheduling model to support trustworthy mixed-criticality real-time systems.</td>
            <td>UNSW</td>
            <td>In progress. Main API stable and available. <em>Note: smaller API changes while verification is in progress.</em></td>
        </tr>
        <tr class="">
            <td>seL4 Microkit</td>
            <td>A simple operating systems framework for building systems on seL4.</td>
            <td>UNSW</td>
            <td>Ongoing research &amp; development. Available for use. Detailed roadmap available <a href="https://github.com/seL4/microkit/issues/61">here</a>.</td>
        </tr>
        <tr class="">
            <td>seL4 Device Driver Framework</td>
            <td>A high-performance and secure driver framework for seL4.</td>
            <td>UNSW</td>
            <td>Ongoing research &amp; development. Available for use. Find out more <a href="https://github.com/au-ts/sddf">here</a>.</td>
        </tr>
        <tr class="">
            <td>LionsOS</td>
            <td>A secure, fast, and adaptable OS based on the seL4 Microkit.</td>
            <td>UNSW</td>
            <td>Ongoing research &amp; development. An initial release containing a non-trivial example system has been made. Find out more <a href="https://lionsos.org">here</a>.</td>
        </tr>
    </tbody>
</table>

<h2 id="verification">Verification</h2>

<!-- Draws content from the "roadmap: section in /_data/projects/<project>.yml -->

<table class="table">
    <thead>
        <tr>
            <th>Feature</th>
            <th>Description</th>
            <th>Assigned</th>
            <th>Status</th>
        </tr>
    </thead>
    <tbody>
        <tr class="">
            <td>MCS Kernel extensions</td>
            <td>Functional correctness proofs for a new scheduling model to support trustworthy mixed-criticality real-time systems.</td>
            <td>Proofcraft</td>
            <td>C verification ongoing</td>
        </tr>
        <tr class="">
            <td>AArch64 port</td>
            <td>Functional correctness proofs for the AArch64 port of seL4 completed. Integrity (access control) ongoing.</td>
            <td>Proofcraft</td>
            <td>Integrity verification to complete Q1/25</td>
        </tr>
    </tbody>
</table>

<h2 id="adding-to-the-roadmap">Adding to the Roadmap</h2>

<p>The roadmap is not only for seL4 kernel development or verification itself.
If you are working on a larger feature or addition to the the wider seL4
ecosystem, and are confident enough to commit to a timeline, you can request
this plan to be added to the roadmap on this page.</p>

<p>If you are contracted to deliver a major user-level component, framework, or
feature in the seL4 ecosystem with a delivery date, and ideally an approved
<a href="../processes/rfc-process">RFC</a> to go with it, your contribution would be
an ideal addition to the roadmap.</p>

<p>A new feature can become a part of the official seL4 roadmap by decision of
the <a href="https://sel4.systems/Foundation/TSC/">Technical Steering Committee</a> (TSC) of the seL4 Foundation. To
submit a request to the TSC for putting a planned feature on the roadmap,
send an email to any TSC member with a description of the contribution, the
planned timeline, and level of confidence for achieving it, e.g. by pointing
to any related RFC. The TSC will discuss the proposal and either request more
information or vote on it.</p>


  </div>

  
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#sel4-development">seL4 Development</a></li>
<li class="toc-entry toc-h2"><a href="#verification">Verification</a></li>
<li class="toc-entry toc-h2"><a href="#adding-to-the-roadmap">Adding to the Roadmap</a></li>
</ul>
</div>

</div>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Thu Nov 11 11:50:06 2021 +1100 318c724114
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/projects/roadmap.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/projects/roadmap.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
